M1, M2:MsgA. M1 || M2  M2 || M1 

latex

Definitions

suptype(S; T), S  T, Valtype(da;k), f || g, ff, P & Q, P  Q, P  Q, if b then t else f fi , {T}, tt, True, b, , P  Q, x. t(x), A c B, f  g, t  T, M1 ||decl M2, t.2, t.1, M1 || M2, P  Q, x:A. B(x), Unit, , SQType(T), A, False, Dec(P), x(s), MsgA,

Lemmas

finite-prob-space wf, IdLnk wf, idlnk-deq wf, rcv wf, ma-valtype wf, subtype-fpf-cap-top, product-deq wf, pi2 wf, pi1 wf, ma-state-subtype, ma-state wf, fpf-sub-join-left, subtype-fpf-cap-void, fpf-cap wf, rationals wf, Kind-deq wf, Knd wf, fpf-ap wf, assert of bnot, eqff to assert, not wf, bnot wf, iff transitivity, eqtt to assert, bool wf, fpf-join-ap, bool sq, assert elim, decidable assert, decidable or, fpf wf, fpf-join-dom, fpf-trivial-subtype-top, top wf, fpf-join wf, id-deq wf, Id wf, fpf-dom wf, assert wf, msga wf, ma-compatible wf